module Spec.Blake2.Test

#reset-options "--z3rlimit 100 --max_fuel 0"

open FStar.Mul
open Lib.IntTypes
open Lib.RawIntTypes
open Lib.Sequence
open Lib.ByteSequence

//
// Test 1
//

let test1_plaintext_list  = List.Tot.map u8_from_UInt8 [
  0x61uy; 0x62uy; 0x63uy
]
let test1_plaintext : lbytes 3 =
  assert_norm (List.Tot.length test1_plaintext_list = 3);
  of_list test1_plaintext_list

let test1_expected_list = List.Tot.map u8_from_UInt8 [
  0x50uy; 0x8Cuy; 0x5Euy; 0x8Cuy; 0x32uy; 0x7Cuy; 0x14uy; 0xE2uy;
  0xE1uy; 0xA7uy; 0x2Buy; 0xA3uy; 0x4Euy; 0xEBuy; 0x45uy; 0x2Fuy;
  0x37uy; 0x45uy; 0x8Buy; 0x20uy; 0x9Euy; 0xD6uy; 0x3Auy; 0x29uy;
  0x4Duy; 0x99uy; 0x9Buy; 0x4Cuy; 0x86uy; 0x67uy; 0x59uy; 0x82uy;
]
let test1_expected : lbytes 32 =
  assert_norm (List.Tot.length test1_expected_list = 32);
  of_list test1_expected_list



let test2_plaintext_list = List.Tot.map u8_from_UInt8 [ 0x00uy ]
let test2_plaintext : lbytes 1 =
  assert_norm (List.Tot.length test2_plaintext_list = 1);
  of_list test2_plaintext_list

let test2_key_list = List.Tot.map u8_from_UInt8 [
  0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy;
  0x08uy; 0x09uy; 0x0auy; 0x0buy; 0x0cuy; 0x0duy; 0x0euy; 0x0fuy;
  0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy;
  0x18uy; 0x19uy; 0x1auy; 0x1buy; 0x1cuy; 0x1duy; 0x1euy; 0x1fuy ]

let test2_key : lbytes 32 =
  assert_norm (List.Tot.length test2_key_list = 32);
  of_list test2_key_list

let test2_expected_list = List.Tot.map u8_from_UInt8 [
  0x40uy; 0xd1uy; 0x5fuy; 0xeeuy; 0x7cuy; 0x32uy; 0x88uy; 0x30uy;
  0x16uy; 0x6auy; 0xc3uy; 0xf9uy; 0x18uy; 0x65uy; 0x0fuy; 0x80uy;
  0x7euy; 0x7euy; 0x01uy; 0xe1uy; 0x77uy; 0x25uy; 0x8cuy; 0xdcuy;
  0x0auy; 0x39uy; 0xb1uy; 0x1fuy; 0x59uy; 0x80uy; 0x66uy; 0xf1uy ]

let test2_expected : lbytes 32 =
  assert_norm (List.Tot.length test2_expected_list = 32);
  of_list test2_expected_list



let test3_plaintext_list = List.Tot.map u8_from_UInt8 [
  0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy;
  0x08uy; 0x09uy; 0x0auy; 0x0buy; 0x0cuy; 0x0duy; 0x0euy; 0x0fuy;
  0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy;
  0x18uy; 0x19uy; 0x1auy; 0x1buy; 0x1cuy; 0x1duy; 0x1euy; 0x1fuy;
  0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy;
  0x28uy; 0x29uy; 0x2auy; 0x2buy; 0x2cuy; 0x2duy; 0x2euy; 0x2fuy;
  0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy;
  0x38uy; 0x39uy; 0x3auy; 0x3buy; 0x3cuy; 0x3duy; 0x3euy; 0x3fuy;
  0x40uy; 0x41uy; 0x42uy; 0x43uy; 0x44uy; 0x45uy; 0x46uy; 0x47uy;
  0x48uy; 0x49uy; 0x4auy; 0x4buy; 0x4cuy; 0x4duy; 0x4euy; 0x4fuy;
  0x50uy; 0x51uy; 0x52uy; 0x53uy; 0x54uy; 0x55uy; 0x56uy; 0x57uy;
  0x58uy; 0x59uy; 0x5auy; 0x5buy; 0x5cuy; 0x5duy; 0x5euy; 0x5fuy;
  0x60uy; 0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy;
  0x68uy; 0x69uy; 0x6auy; 0x6buy; 0x6cuy; 0x6duy; 0x6euy; 0x6fuy;
  0x70uy; 0x71uy; 0x72uy; 0x73uy; 0x74uy; 0x75uy; 0x76uy; 0x77uy;
  0x78uy; 0x79uy; 0x7auy; 0x7buy; 0x7cuy; 0x7duy; 0x7euy; 0x7fuy;
  0x80uy; 0x81uy; 0x82uy; 0x83uy; 0x84uy; 0x85uy; 0x86uy; 0x87uy;
  0x88uy; 0x89uy; 0x8auy; 0x8buy; 0x8cuy; 0x8duy; 0x8euy; 0x8fuy;
  0x90uy; 0x91uy; 0x92uy; 0x93uy; 0x94uy; 0x95uy; 0x96uy; 0x97uy;
  0x98uy; 0x99uy; 0x9auy; 0x9buy; 0x9cuy; 0x9duy; 0x9euy; 0x9fuy;
  0xa0uy; 0xa1uy; 0xa2uy; 0xa3uy; 0xa4uy; 0xa5uy; 0xa6uy; 0xa7uy;
  0xa8uy; 0xa9uy; 0xaauy; 0xabuy; 0xacuy; 0xaduy; 0xaeuy; 0xafuy;
  0xb0uy; 0xb1uy; 0xb2uy; 0xb3uy; 0xb4uy; 0xb5uy; 0xb6uy; 0xb7uy;
  0xb8uy; 0xb9uy; 0xbauy; 0xbbuy; 0xbcuy; 0xbduy; 0xbeuy; 0xbfuy;
  0xc0uy; 0xc1uy; 0xc2uy; 0xc3uy; 0xc4uy; 0xc5uy; 0xc6uy; 0xc7uy;
  0xc8uy; 0xc9uy; 0xcauy; 0xcbuy; 0xccuy; 0xcduy; 0xceuy; 0xcfuy;
  0xd0uy; 0xd1uy; 0xd2uy; 0xd3uy; 0xd4uy; 0xd5uy; 0xd6uy; 0xd7uy;
  0xd8uy; 0xd9uy; 0xdauy; 0xdbuy; 0xdcuy; 0xdduy; 0xdeuy; 0xdfuy;
  0xe0uy; 0xe1uy; 0xe2uy; 0xe3uy; 0xe4uy; 0xe5uy; 0xe6uy; 0xe7uy;
  0xe8uy; 0xe9uy; 0xeauy; 0xebuy; 0xecuy; 0xeduy; 0xeeuy; 0xefuy;
  0xf0uy; 0xf1uy; 0xf2uy; 0xf3uy; 0xf4uy; 0xf5uy; 0xf6uy; 0xf7uy;
  0xf8uy; 0xf9uy; 0xfauy; 0xfbuy; 0xfcuy; 0xfduy; 0xfeuy
]

let test3_plaintext : lbytes 255 =
  assert_norm (List.Tot.length test3_plaintext_list = 255);
  of_list test3_plaintext_list

let test3_key_list = List.Tot.map u8_from_UInt8 [
  0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy;
  0x08uy; 0x09uy; 0x0auy; 0x0buy; 0x0cuy; 0x0duy; 0x0euy; 0x0fuy;
  0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy;
  0x18uy; 0x19uy; 0x1auy; 0x1buy; 0x1cuy; 0x1duy; 0x1euy; 0x1fuy ]

let test3_key : lbytes 32 =
  assert_norm (List.Tot.length test3_key_list = 32);
  of_list test3_key_list

let test3_expected_list = List.Tot.map u8_from_UInt8 [
  0x3fuy; 0xb7uy; 0x35uy; 0x06uy; 0x1auy; 0xbcuy; 0x51uy; 0x9duy;
  0xfeuy; 0x97uy; 0x9euy; 0x54uy; 0xc1uy; 0xeeuy; 0x5buy; 0xfauy;
  0xd0uy; 0xa9uy; 0xd8uy; 0x58uy; 0xb3uy; 0x31uy; 0x5buy; 0xaduy;
  0x34uy; 0xbduy; 0xe9uy; 0x99uy; 0xefuy; 0xd7uy; 0x24uy; 0xdduy ]

let test3_expected : lbytes 32 =
  assert_norm (List.Tot.length test3_expected_list = 32);
  of_list test3_expected_list



let test4_plaintext_list = List.Tot.map u8_from_UInt8 [
  0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy;
  0x08uy; 0x09uy; 0x0auy; 0x0buy; 0x0cuy; 0x0duy; 0x0euy; 0x0fuy;
  0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy;
  0x18uy; 0x19uy; 0x1auy; 0x1buy; 0x1cuy; 0x1duy; 0x1euy; 0x1fuy;
  0x20uy; 0x21uy; 0x22uy; 0x23uy; 0x24uy; 0x25uy; 0x26uy; 0x27uy;
  0x28uy; 0x29uy; 0x2auy; 0x2buy; 0x2cuy; 0x2duy; 0x2euy; 0x2fuy;
  0x30uy; 0x31uy; 0x32uy; 0x33uy; 0x34uy; 0x35uy; 0x36uy; 0x37uy;
  0x38uy; 0x39uy; 0x3auy; 0x3buy; 0x3cuy; 0x3duy; 0x3euy; 0x3fuy;
  0x40uy; 0x41uy; 0x42uy; 0x43uy; 0x44uy; 0x45uy; 0x46uy; 0x47uy;
  0x48uy; 0x49uy; 0x4auy; 0x4buy; 0x4cuy; 0x4duy; 0x4euy; 0x4fuy;
  0x50uy; 0x51uy; 0x52uy; 0x53uy; 0x54uy; 0x55uy; 0x56uy; 0x57uy;
  0x58uy; 0x59uy; 0x5auy; 0x5buy; 0x5cuy; 0x5duy; 0x5euy; 0x5fuy;
  0x60uy; 0x61uy; 0x62uy; 0x63uy; 0x64uy; 0x65uy; 0x66uy; 0x67uy;
  0x68uy; 0x69uy; 0x6auy; 0x6buy; 0x6cuy; 0x6duy; 0x6euy; 0x6fuy;
  0x70uy; 0x71uy; 0x72uy; 0x73uy; 0x74uy; 0x75uy; 0x76uy; 0x77uy;
  0x78uy; 0x79uy; 0x7auy; 0x7buy; 0x7cuy; 0x7duy; 0x7euy; 0x7fuy;
  0x80uy; 0x81uy; 0x82uy; 0x83uy; 0x84uy; 0x85uy; 0x86uy; 0x87uy;
  0x88uy; 0x89uy; 0x8auy; 0x8buy; 0x8cuy; 0x8duy; 0x8euy; 0x8fuy;
  0x90uy; 0x91uy; 0x92uy; 0x93uy; 0x94uy; 0x95uy; 0x96uy; 0x97uy;
  0x98uy; 0x99uy; 0x9auy; 0x9buy; 0x9cuy; 0x9duy; 0x9euy; 0x9fuy;
  0xa0uy; 0xa1uy; 0xa2uy; 0xa3uy; 0xa4uy; 0xa5uy; 0xa6uy; 0xa7uy;
  0xa8uy; 0xa9uy; 0xaauy; 0xabuy; 0xacuy; 0xaduy; 0xaeuy; 0xafuy;
  0xb0uy; 0xb1uy; 0xb2uy; 0xb3uy; 0xb4uy; 0xb5uy; 0xb6uy; 0xb7uy;
  0xb8uy; 0xb9uy; 0xbauy; 0xbbuy; 0xbcuy; 0xbduy; 0xbeuy; 0xbfuy;
  0xc0uy; 0xc1uy; 0xc2uy; 0xc3uy; 0xc4uy; 0xc5uy; 0xc6uy; 0xc7uy;
  0xc8uy; 0xc9uy; 0xcauy; 0xcbuy; 0xccuy; 0xcduy; 0xceuy; 0xcfuy;
  0xd0uy; 0xd1uy; 0xd2uy; 0xd3uy; 0xd4uy; 0xd5uy; 0xd6uy; 0xd7uy;
  0xd8uy; 0xd9uy; 0xdauy; 0xdbuy; 0xdcuy; 0xdduy; 0xdeuy; 0xdfuy;
  0xe0uy; 0xe1uy; 0xe2uy; 0xe3uy; 0xe4uy; 0xe5uy; 0xe6uy; 0xe7uy;
  0xe8uy; 0xe9uy; 0xeauy; 0xebuy; 0xecuy; 0xeduy; 0xeeuy; 0xefuy;
  0xf0uy; 0xf1uy; 0xf2uy; 0xf3uy; 0xf4uy; 0xf5uy; 0xf6uy; 0xf7uy;
  0xf8uy; 0xf9uy; 0xfauy
]

let test4_plaintext : lbytes 251 =
  assert_norm (List.Tot.length test4_plaintext_list = 251);
  of_list test4_plaintext_list

let test4_key_list = List.Tot.map u8_from_UInt8 [
  0x00uy; 0x01uy; 0x02uy; 0x03uy; 0x04uy; 0x05uy; 0x06uy; 0x07uy;
  0x08uy; 0x09uy; 0x0auy; 0x0buy; 0x0cuy; 0x0duy; 0x0euy; 0x0fuy;
  0x10uy; 0x11uy; 0x12uy; 0x13uy; 0x14uy; 0x15uy; 0x16uy; 0x17uy;
  0x18uy; 0x19uy; 0x1auy; 0x1buy; 0x1cuy; 0x1duy; 0x1euy; 0x1fuy ]

let test4_key : lbytes 32 =
  assert_norm (List.Tot.length test4_key_list = 32);
  of_list test4_key_list

let test4_expected_list = List.Tot.map u8_from_UInt8 [
  0xd1uy; 0x2buy; 0xf3uy; 0x73uy; 0x2euy; 0xf4uy; 0xafuy; 0x5cuy;
  0x22uy; 0xfauy; 0x90uy; 0x35uy; 0x6auy; 0xf8uy; 0xfcuy; 0x50uy;
  0xfcuy; 0xb4uy; 0x0fuy; 0x8fuy; 0x2euy; 0xa5uy; 0xc8uy; 0x59uy;
  0x47uy; 0x37uy; 0xa3uy; 0xb3uy; 0xd5uy; 0xabuy; 0xdbuy; 0xd7uy
]

let test4_expected : lbytes 32 =
  assert_norm (List.Tot.length test4_expected_list = 32);
  of_list test4_expected_list







//
// Test 5 BLAKE 2B
//

let test5_plaintext_list  = List.Tot.map u8_from_UInt8 [
  0x61uy; 0x62uy; 0x63uy
]
let test5_plaintext : lbytes 3 =
  assert_norm (List.Tot.length test5_plaintext_list = 3);
  of_list test5_plaintext_list

let test5_expected_list = List.Tot.map u8_from_UInt8 [
  0xBAuy; 0x80uy; 0xA5uy; 0x3Fuy; 0x98uy; 0x1Cuy; 0x4Duy; 0x0Duy; 0x6Auy; 0x27uy; 0x97uy; 0xB6uy; 0x9Fuy; 0x12uy; 0xF6uy; 0xE9uy;
  0x4Cuy; 0x21uy; 0x2Fuy; 0x14uy; 0x68uy; 0x5Auy; 0xC4uy; 0xB7uy; 0x4Buy; 0x12uy; 0xBBuy; 0x6Fuy; 0xDBuy; 0xFFuy; 0xA2uy; 0xD1uy;
  0x7Duy; 0x87uy; 0xC5uy; 0x39uy; 0x2Auy; 0xABuy; 0x79uy; 0x2Duy; 0xC2uy; 0x52uy; 0xD5uy; 0xDEuy; 0x45uy; 0x33uy; 0xCCuy; 0x95uy;
  0x18uy; 0xD3uy; 0x8Auy; 0xA8uy; 0xDBuy; 0xF1uy; 0x92uy; 0x5Auy; 0xB9uy; 0x23uy; 0x86uy; 0xEDuy; 0xD4uy; 0x00uy; 0x99uy; 0x23uy
]
let test5_expected : lbytes 64 =
  assert_norm (List.Tot.length test5_expected_list = 64);
  of_list test5_expected_list


//
// Test 6 BLAKE 2B
//

let test6_plaintext_list  = List.Tot.map u8_from_UInt8 [
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy
]

let test6_plaintext : lbytes 128 =
  assert_norm (List.Tot.length test6_plaintext_list = 128);
  of_list test6_plaintext_list

let test6_key_list  = List.Tot.map u8_from_UInt8 [
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy;
  0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy; 0x00uy
]

let test6_key : lbytes 64 =
  assert_norm (List.Tot.length test6_key_list = 64);
  of_list test6_key_list

let test6_expected_list = List.Tot.map u8_from_UInt8 [
  0xe4uy; 0x7buy; 0xb6uy; 0xf2uy; 0x0fuy; 0xbfuy; 0x14uy; 0x98uy;
  0x4fuy; 0x72uy; 0xa4uy; 0xc3uy; 0xcduy; 0x9fuy; 0x3duy; 0xc0uy;
  0xd3uy; 0x89uy; 0x28uy; 0xe5uy; 0x36uy; 0x73uy; 0x3buy; 0xa7uy;
  0xc5uy; 0xb1uy; 0x53uy; 0xc7uy; 0x15uy; 0x46uy; 0x58uy; 0x4buy;
  0x73uy; 0x71uy; 0xf9uy; 0xb7uy; 0x07uy; 0x07uy; 0x77uy; 0xb9uy;
  0xa0uy; 0x94uy; 0x77uy; 0x03uy; 0x40uy; 0x96uy; 0x50uy; 0xfduy;
  0x04uy; 0xcfuy; 0xc9uy; 0xa5uy; 0xd5uy; 0x61uy; 0xf9uy; 0x9euy;
  0xd1uy; 0x34uy; 0xefuy; 0x26uy; 0x2buy; 0x03uy; 0xdbuy; 0x94uy
]

let test6_expected : lbytes 64 =
  assert_norm (List.Tot.length test6_expected_list = 64);
  of_list test6_expected_list


(*** Blake2s test vectors: *)

(* test7_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E" *)
let test7_plaintext_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy;  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy; 
  0x28uy;  0x29uy;  0x2Auy;  0x2Buy;  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy; 
  0x32uy;  0x33uy;  0x34uy;  0x35uy;  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy; 
  0x3Cuy;  0x3Duy;  0x3Euy ]

let test7_plaintext : lbytes 63 =
  assert_norm(FStar.List.length test7_plaintext_list = 63);
  of_list test7_plaintext_list

(* test7_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F" *)
let test7_key_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy ]

let test7_key : lbytes 32 =
  assert_norm(FStar.List.length test7_key_list = 32);
  of_list test7_key_list

(* test7_expected = "C65382513F07460DA39833CB666C5ED82E61B9E998F4B0C4287CEE56C3CC9BCD" *)
let test7_expected_list = List.Tot.map u8_from_UInt8 [
  0xC6uy;  0x53uy;  0x82uy;  0x51uy;  0x3Fuy;  0x07uy;  0x46uy;  0x0Duy;  0xA3uy;  0x98uy; 
  0x33uy;  0xCBuy;  0x66uy;  0x6Cuy;  0x5Euy;  0xD8uy;  0x2Euy;  0x61uy;  0xB9uy;  0xE9uy; 
  0x98uy;  0xF4uy;  0xB0uy;  0xC4uy;  0x28uy;  0x7Cuy;  0xEEuy;  0x56uy;  0xC3uy;  0xCCuy; 
  0x9Buy;  0xCDuy ]

let test7_expected : lbytes 32 =
  assert_norm(FStar.List.length test7_expected_list = 32);
  of_list test7_expected_list

(* test8_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F" *)
let test8_plaintext_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy;  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy; 
  0x28uy;  0x29uy;  0x2Auy;  0x2Buy;  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy; 
  0x32uy;  0x33uy;  0x34uy;  0x35uy;  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy; 
  0x3Cuy;  0x3Duy;  0x3Euy;  0x3Fuy ]

let test8_plaintext : lbytes 64 =
  assert_norm(FStar.List.length test8_plaintext_list = 64);
  of_list test8_plaintext_list

(* test8_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F" *)
let test8_key_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy ]

let test8_key : lbytes 32 =
  assert_norm(FStar.List.length test8_key_list = 32);
  of_list test8_key_list

(* test8_expected = "8975B0577FD35566D750B362B0897A26C399136DF07BABABBDE6203FF2954ED4" *)
let test8_expected_list = List.Tot.map u8_from_UInt8 [
  0x89uy;  0x75uy;  0xB0uy;  0x57uy;  0x7Fuy;  0xD3uy;  0x55uy;  0x66uy;  0xD7uy;  0x50uy; 
  0xB3uy;  0x62uy;  0xB0uy;  0x89uy;  0x7Auy;  0x26uy;  0xC3uy;  0x99uy;  0x13uy;  0x6Duy; 
  0xF0uy;  0x7Buy;  0xABuy;  0xABuy;  0xBDuy;  0xE6uy;  0x20uy;  0x3Fuy;  0xF2uy;  0x95uy; 
  0x4Euy;  0xD4uy ]

let test8_expected : lbytes 32 =
  assert_norm(FStar.List.length test8_expected_list = 32);
  of_list test8_expected_list

(* test9_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F40" *)
let test9_plaintext_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy;  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy; 
  0x28uy;  0x29uy;  0x2Auy;  0x2Buy;  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy; 
  0x32uy;  0x33uy;  0x34uy;  0x35uy;  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy; 
  0x3Cuy;  0x3Duy;  0x3Euy;  0x3Fuy;  0x40uy ]

let test9_plaintext : lbytes 65 =
  assert_norm(FStar.List.length test9_plaintext_list = 65);
  of_list test9_plaintext_list

(* test9_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F" *)
let test9_key_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy ]

let test9_key : lbytes 32 =
  assert_norm(FStar.List.length test9_key_list = 32);
  of_list test9_key_list

(* test9_expected = "21FE0CEB0052BE7FB0F004187CACD7DE67FA6EB0938D927677F2398C132317A8" *)
let test9_expected_list = List.Tot.map u8_from_UInt8 [
  0x21uy;  0xFEuy;  0x0Cuy;  0xEBuy;  0x00uy;  0x52uy;  0xBEuy;  0x7Fuy;  0xB0uy;  0xF0uy; 
  0x04uy;  0x18uy;  0x7Cuy;  0xACuy;  0xD7uy;  0xDEuy;  0x67uy;  0xFAuy;  0x6Euy;  0xB0uy; 
  0x93uy;  0x8Duy;  0x92uy;  0x76uy;  0x77uy;  0xF2uy;  0x39uy;  0x8Cuy;  0x13uy;  0x23uy; 
  0x17uy;  0xA8uy ]

let test9_expected : lbytes 32 =
  assert_norm(FStar.List.length test9_expected_list = 32);
  of_list test9_expected_list

(* test10_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E7F" *)
let test10_plaintext_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy;  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy; 
  0x28uy;  0x29uy;  0x2Auy;  0x2Buy;  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy; 
  0x32uy;  0x33uy;  0x34uy;  0x35uy;  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy; 
  0x3Cuy;  0x3Duy;  0x3Euy;  0x3Fuy;  0x40uy;  0x41uy;  0x42uy;  0x43uy;  0x44uy;  0x45uy; 
  0x46uy;  0x47uy;  0x48uy;  0x49uy;  0x4Auy;  0x4Buy;  0x4Cuy;  0x4Duy;  0x4Euy;  0x4Fuy; 
  0x50uy;  0x51uy;  0x52uy;  0x53uy;  0x54uy;  0x55uy;  0x56uy;  0x57uy;  0x58uy;  0x59uy; 
  0x5Auy;  0x5Buy;  0x5Cuy;  0x5Duy;  0x5Euy;  0x5Fuy;  0x60uy;  0x61uy;  0x62uy;  0x63uy; 
  0x64uy;  0x65uy;  0x66uy;  0x67uy;  0x68uy;  0x69uy;  0x6Auy;  0x6Buy;  0x6Cuy;  0x6Duy; 
  0x6Euy;  0x6Fuy;  0x70uy;  0x71uy;  0x72uy;  0x73uy;  0x74uy;  0x75uy;  0x76uy;  0x77uy; 
  0x78uy;  0x79uy;  0x7Auy;  0x7Buy;  0x7Cuy;  0x7Duy;  0x7Euy;  0x7Fuy ]

let test10_plaintext : lbytes 128 =
  assert_norm(FStar.List.length test10_plaintext_list = 128);
  of_list test10_plaintext_list

(* test10_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F" *)
let test10_key_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy ]

let test10_key : lbytes 32 =
  assert_norm(FStar.List.length test10_key_list = 32);
  of_list test10_key_list

(* test10_expected = "0C311F38C35A4FB90D651C289D486856CD1413DF9B0677F53ECE2CD9E477C60A" *)
let test10_expected_list = List.Tot.map u8_from_UInt8 [
  0x0Cuy;  0x31uy;  0x1Fuy;  0x38uy;  0xC3uy;  0x5Auy;  0x4Fuy;  0xB9uy;  0x0Duy;  0x65uy; 
  0x1Cuy;  0x28uy;  0x9Duy;  0x48uy;  0x68uy;  0x56uy;  0xCDuy;  0x14uy;  0x13uy;  0xDFuy; 
  0x9Buy;  0x06uy;  0x77uy;  0xF5uy;  0x3Euy;  0xCEuy;  0x2Cuy;  0xD9uy;  0xE4uy;  0x77uy; 
  0xC6uy;  0x0Auy ]

let test10_expected : lbytes 32 =
  assert_norm(FStar.List.length test10_expected_list = 32);
  of_list test10_expected_list

(* test11_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E7F808182838485868788898A8B8C8D8E8F909192939495969798999A9B9C9D9E9FA0A1A2A3A4A5A6A7A8A9AAABACADAEAFB0B1B2B3B4B5B6B7B8B9BABBBCBDBEBFC0C1C2C3C4C5C6C7C8C9CACBCCCDCECFD0D1D2D3D4D5D6D7D8D9DADBDCDDDEDFE0E1E2E3E4E5E6E7E8E9EAEBECEDEEEFF0F1F2F3F4F5F6F7F8F9FAFBFCFDFEFF" *)
let test11_plaintext_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy;  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy; 
  0x28uy;  0x29uy;  0x2Auy;  0x2Buy;  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy; 
  0x32uy;  0x33uy;  0x34uy;  0x35uy;  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy; 
  0x3Cuy;  0x3Duy;  0x3Euy;  0x3Fuy;  0x40uy;  0x41uy;  0x42uy;  0x43uy;  0x44uy;  0x45uy; 
  0x46uy;  0x47uy;  0x48uy;  0x49uy;  0x4Auy;  0x4Buy;  0x4Cuy;  0x4Duy;  0x4Euy;  0x4Fuy; 
  0x50uy;  0x51uy;  0x52uy;  0x53uy;  0x54uy;  0x55uy;  0x56uy;  0x57uy;  0x58uy;  0x59uy; 
  0x5Auy;  0x5Buy;  0x5Cuy;  0x5Duy;  0x5Euy;  0x5Fuy;  0x60uy;  0x61uy;  0x62uy;  0x63uy; 
  0x64uy;  0x65uy;  0x66uy;  0x67uy;  0x68uy;  0x69uy;  0x6Auy;  0x6Buy;  0x6Cuy;  0x6Duy; 
  0x6Euy;  0x6Fuy;  0x70uy;  0x71uy;  0x72uy;  0x73uy;  0x74uy;  0x75uy;  0x76uy;  0x77uy; 
  0x78uy;  0x79uy;  0x7Auy;  0x7Buy;  0x7Cuy;  0x7Duy;  0x7Euy;  0x7Fuy;  0x80uy;  0x81uy; 
  0x82uy;  0x83uy;  0x84uy;  0x85uy;  0x86uy;  0x87uy;  0x88uy;  0x89uy;  0x8Auy;  0x8Buy; 
  0x8Cuy;  0x8Duy;  0x8Euy;  0x8Fuy;  0x90uy;  0x91uy;  0x92uy;  0x93uy;  0x94uy;  0x95uy; 
  0x96uy;  0x97uy;  0x98uy;  0x99uy;  0x9Auy;  0x9Buy;  0x9Cuy;  0x9Duy;  0x9Euy;  0x9Fuy; 
  0xA0uy;  0xA1uy;  0xA2uy;  0xA3uy;  0xA4uy;  0xA5uy;  0xA6uy;  0xA7uy;  0xA8uy;  0xA9uy; 
  0xAAuy;  0xABuy;  0xACuy;  0xADuy;  0xAEuy;  0xAFuy;  0xB0uy;  0xB1uy;  0xB2uy;  0xB3uy; 
  0xB4uy;  0xB5uy;  0xB6uy;  0xB7uy;  0xB8uy;  0xB9uy;  0xBAuy;  0xBBuy;  0xBCuy;  0xBDuy; 
  0xBEuy;  0xBFuy;  0xC0uy;  0xC1uy;  0xC2uy;  0xC3uy;  0xC4uy;  0xC5uy;  0xC6uy;  0xC7uy; 
  0xC8uy;  0xC9uy;  0xCAuy;  0xCBuy;  0xCCuy;  0xCDuy;  0xCEuy;  0xCFuy;  0xD0uy;  0xD1uy; 
  0xD2uy;  0xD3uy;  0xD4uy;  0xD5uy;  0xD6uy;  0xD7uy;  0xD8uy;  0xD9uy;  0xDAuy;  0xDBuy; 
  0xDCuy;  0xDDuy;  0xDEuy;  0xDFuy;  0xE0uy;  0xE1uy;  0xE2uy;  0xE3uy;  0xE4uy;  0xE5uy; 
  0xE6uy;  0xE7uy;  0xE8uy;  0xE9uy;  0xEAuy;  0xEBuy;  0xECuy;  0xEDuy;  0xEEuy;  0xEFuy; 
  0xF0uy;  0xF1uy;  0xF2uy;  0xF3uy;  0xF4uy;  0xF5uy;  0xF6uy;  0xF7uy;  0xF8uy;  0xF9uy; 
  0xFAuy;  0xFBuy;  0xFCuy;  0xFDuy;  0xFEuy;  0xFFuy ]

let test11_plaintext : lbytes 256 =
  assert_norm(FStar.List.length test11_plaintext_list = 256);
  of_list test11_plaintext_list

(* test11_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F" *)
let test11_key_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy ]

let test11_key : lbytes 32 =
  assert_norm(FStar.List.length test11_key_list = 32);
  of_list test11_key_list

(* test11_expected = "5211D1AEFC0025BE7F85C06B3E14E0FC645AE12BD41746485EA6D8A364A2EAEE" *)
let test11_expected_list = List.Tot.map u8_from_UInt8 [
  0x52uy;  0x11uy;  0xD1uy;  0xAEuy;  0xFCuy;  0x00uy;  0x25uy;  0xBEuy;  0x7Fuy;  0x85uy; 
  0xC0uy;  0x6Buy;  0x3Euy;  0x14uy;  0xE0uy;  0xFCuy;  0x64uy;  0x5Auy;  0xE1uy;  0x2Buy; 
  0xD4uy;  0x17uy;  0x46uy;  0x48uy;  0x5Euy;  0xA6uy;  0xD8uy;  0xA3uy;  0x64uy;  0xA2uy; 
  0xEAuy;  0xEEuy ]

let test11_expected : lbytes 32 =
  assert_norm(FStar.List.length test11_expected_list = 32);
  of_list test11_expected_list

(*** Blake2b test vectors: *)

(* test12_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E" *)
let test12_plaintext_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy;  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy; 
  0x28uy;  0x29uy;  0x2Auy;  0x2Buy;  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy; 
  0x32uy;  0x33uy;  0x34uy;  0x35uy;  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy; 
  0x3Cuy;  0x3Duy;  0x3Euy;  0x3Fuy;  0x40uy;  0x41uy;  0x42uy;  0x43uy;  0x44uy;  0x45uy; 
  0x46uy;  0x47uy;  0x48uy;  0x49uy;  0x4Auy;  0x4Buy;  0x4Cuy;  0x4Duy;  0x4Euy;  0x4Fuy; 
  0x50uy;  0x51uy;  0x52uy;  0x53uy;  0x54uy;  0x55uy;  0x56uy;  0x57uy;  0x58uy;  0x59uy; 
  0x5Auy;  0x5Buy;  0x5Cuy;  0x5Duy;  0x5Euy;  0x5Fuy;  0x60uy;  0x61uy;  0x62uy;  0x63uy; 
  0x64uy;  0x65uy;  0x66uy;  0x67uy;  0x68uy;  0x69uy;  0x6Auy;  0x6Buy;  0x6Cuy;  0x6Duy; 
  0x6Euy;  0x6Fuy;  0x70uy;  0x71uy;  0x72uy;  0x73uy;  0x74uy;  0x75uy;  0x76uy;  0x77uy; 
  0x78uy;  0x79uy;  0x7Auy;  0x7Buy;  0x7Cuy;  0x7Duy;  0x7Euy ]

let test12_plaintext : lbytes 127 =
  assert_norm(FStar.List.length test12_plaintext_list = 127);
  of_list test12_plaintext_list

(* test12_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F" *)
let test12_key_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy;  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy; 
  0x28uy;  0x29uy;  0x2Auy;  0x2Buy;  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy; 
  0x32uy;  0x33uy;  0x34uy;  0x35uy;  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy; 
  0x3Cuy;  0x3Duy;  0x3Euy;  0x3Fuy ]

let test12_key : lbytes 64 =
  assert_norm(FStar.List.length test12_key_list = 64);
  of_list test12_key_list

(* test12_expected = "76D2D819C92BCE55FA8E092AB1BF9B9EAB237A25267986CACF2B8EE14D214D730DC9A5AA2D7B596E86A1FD8FA0804C77402D2FCD45083688B218B1CDFA0DCBCB" *)
let test12_expected_list = List.Tot.map u8_from_UInt8 [
  0x76uy;  0xD2uy;  0xD8uy;  0x19uy;  0xC9uy;  0x2Buy;  0xCEuy;  0x55uy;  0xFAuy;  0x8Euy; 
  0x09uy;  0x2Auy;  0xB1uy;  0xBFuy;  0x9Buy;  0x9Euy;  0xABuy;  0x23uy;  0x7Auy;  0x25uy; 
  0x26uy;  0x79uy;  0x86uy;  0xCAuy;  0xCFuy;  0x2Buy;  0x8Euy;  0xE1uy;  0x4Duy;  0x21uy; 
  0x4Duy;  0x73uy;  0x0Duy;  0xC9uy;  0xA5uy;  0xAAuy;  0x2Duy;  0x7Buy;  0x59uy;  0x6Euy; 
  0x86uy;  0xA1uy;  0xFDuy;  0x8Fuy;  0xA0uy;  0x80uy;  0x4Cuy;  0x77uy;  0x40uy;  0x2Duy; 
  0x2Fuy;  0xCDuy;  0x45uy;  0x08uy;  0x36uy;  0x88uy;  0xB2uy;  0x18uy;  0xB1uy;  0xCDuy; 
  0xFAuy;  0x0Duy;  0xCBuy;  0xCBuy ]

let test12_expected : lbytes 64 =
  assert_norm(FStar.List.length test12_expected_list = 64);
  of_list test12_expected_list

(* test13_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E7F" *)
let test13_plaintext_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy;  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy; 
  0x28uy;  0x29uy;  0x2Auy;  0x2Buy;  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy; 
  0x32uy;  0x33uy;  0x34uy;  0x35uy;  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy; 
  0x3Cuy;  0x3Duy;  0x3Euy;  0x3Fuy;  0x40uy;  0x41uy;  0x42uy;  0x43uy;  0x44uy;  0x45uy; 
  0x46uy;  0x47uy;  0x48uy;  0x49uy;  0x4Auy;  0x4Buy;  0x4Cuy;  0x4Duy;  0x4Euy;  0x4Fuy; 
  0x50uy;  0x51uy;  0x52uy;  0x53uy;  0x54uy;  0x55uy;  0x56uy;  0x57uy;  0x58uy;  0x59uy; 
  0x5Auy;  0x5Buy;  0x5Cuy;  0x5Duy;  0x5Euy;  0x5Fuy;  0x60uy;  0x61uy;  0x62uy;  0x63uy; 
  0x64uy;  0x65uy;  0x66uy;  0x67uy;  0x68uy;  0x69uy;  0x6Auy;  0x6Buy;  0x6Cuy;  0x6Duy; 
  0x6Euy;  0x6Fuy;  0x70uy;  0x71uy;  0x72uy;  0x73uy;  0x74uy;  0x75uy;  0x76uy;  0x77uy; 
  0x78uy;  0x79uy;  0x7Auy;  0x7Buy;  0x7Cuy;  0x7Duy;  0x7Euy;  0x7Fuy ]

let test13_plaintext : lbytes 128 =
  assert_norm(FStar.List.length test13_plaintext_list = 128);
  of_list test13_plaintext_list

(* test13_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F" *)
let test13_key_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy;  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy; 
  0x28uy;  0x29uy;  0x2Auy;  0x2Buy;  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy; 
  0x32uy;  0x33uy;  0x34uy;  0x35uy;  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy; 
  0x3Cuy;  0x3Duy;  0x3Euy;  0x3Fuy ]

let test13_key : lbytes 64 =
  assert_norm(FStar.List.length test13_key_list = 64);
  of_list test13_key_list

(* test13_expected = "72065EE4DD91C2D8509FA1FC28A37C7FC9FA7D5B3F8AD3D0D7A25626B57B1B44788D4CAF806290425F9890A3A2A35A905AB4B37ACFD0DA6E4517B2525C9651E4" *)
let test13_expected_list = List.Tot.map u8_from_UInt8 [
  0x72uy;  0x06uy;  0x5Euy;  0xE4uy;  0xDDuy;  0x91uy;  0xC2uy;  0xD8uy;  0x50uy;  0x9Fuy; 
  0xA1uy;  0xFCuy;  0x28uy;  0xA3uy;  0x7Cuy;  0x7Fuy;  0xC9uy;  0xFAuy;  0x7Duy;  0x5Buy; 
  0x3Fuy;  0x8Auy;  0xD3uy;  0xD0uy;  0xD7uy;  0xA2uy;  0x56uy;  0x26uy;  0xB5uy;  0x7Buy; 
  0x1Buy;  0x44uy;  0x78uy;  0x8Duy;  0x4Cuy;  0xAFuy;  0x80uy;  0x62uy;  0x90uy;  0x42uy; 
  0x5Fuy;  0x98uy;  0x90uy;  0xA3uy;  0xA2uy;  0xA3uy;  0x5Auy;  0x90uy;  0x5Auy;  0xB4uy; 
  0xB3uy;  0x7Auy;  0xCFuy;  0xD0uy;  0xDAuy;  0x6Euy;  0x45uy;  0x17uy;  0xB2uy;  0x52uy; 
  0x5Cuy;  0x96uy;  0x51uy;  0xE4uy ]

let test13_expected : lbytes 64 =
  assert_norm(FStar.List.length test13_expected_list = 64);
  of_list test13_expected_list

(* test14_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E7F80" *)
let test14_plaintext_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy;  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy; 
  0x28uy;  0x29uy;  0x2Auy;  0x2Buy;  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy; 
  0x32uy;  0x33uy;  0x34uy;  0x35uy;  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy; 
  0x3Cuy;  0x3Duy;  0x3Euy;  0x3Fuy;  0x40uy;  0x41uy;  0x42uy;  0x43uy;  0x44uy;  0x45uy; 
  0x46uy;  0x47uy;  0x48uy;  0x49uy;  0x4Auy;  0x4Buy;  0x4Cuy;  0x4Duy;  0x4Euy;  0x4Fuy; 
  0x50uy;  0x51uy;  0x52uy;  0x53uy;  0x54uy;  0x55uy;  0x56uy;  0x57uy;  0x58uy;  0x59uy; 
  0x5Auy;  0x5Buy;  0x5Cuy;  0x5Duy;  0x5Euy;  0x5Fuy;  0x60uy;  0x61uy;  0x62uy;  0x63uy; 
  0x64uy;  0x65uy;  0x66uy;  0x67uy;  0x68uy;  0x69uy;  0x6Auy;  0x6Buy;  0x6Cuy;  0x6Duy; 
  0x6Euy;  0x6Fuy;  0x70uy;  0x71uy;  0x72uy;  0x73uy;  0x74uy;  0x75uy;  0x76uy;  0x77uy; 
  0x78uy;  0x79uy;  0x7Auy;  0x7Buy;  0x7Cuy;  0x7Duy;  0x7Euy;  0x7Fuy;  0x80uy ]

let test14_plaintext : lbytes 129 =
  assert_norm(FStar.List.length test14_plaintext_list = 129);
  of_list test14_plaintext_list

(* test14_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F" *)
let test14_key_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy;  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy; 
  0x28uy;  0x29uy;  0x2Auy;  0x2Buy;  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy; 
  0x32uy;  0x33uy;  0x34uy;  0x35uy;  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy; 
  0x3Cuy;  0x3Duy;  0x3Euy;  0x3Fuy ]

let test14_key : lbytes 64 =
  assert_norm(FStar.List.length test14_key_list = 64);
  of_list test14_key_list

(* test14_expected = "64475DFE7600D7171BEA0B394E27C9B00D8E74DD1E416A79473682AD3DFDBB706631558055CFC8A40E07BD015A4540DCDEA15883CBBF31412DF1DE1CD4152B91" *)
let test14_expected_list = List.Tot.map u8_from_UInt8 [
  0x64uy;  0x47uy;  0x5Duy;  0xFEuy;  0x76uy;  0x00uy;  0xD7uy;  0x17uy;  0x1Buy;  0xEAuy; 
  0x0Buy;  0x39uy;  0x4Euy;  0x27uy;  0xC9uy;  0xB0uy;  0x0Duy;  0x8Euy;  0x74uy;  0xDDuy; 
  0x1Euy;  0x41uy;  0x6Auy;  0x79uy;  0x47uy;  0x36uy;  0x82uy;  0xADuy;  0x3Duy;  0xFDuy; 
  0xBBuy;  0x70uy;  0x66uy;  0x31uy;  0x55uy;  0x80uy;  0x55uy;  0xCFuy;  0xC8uy;  0xA4uy; 
  0x0Euy;  0x07uy;  0xBDuy;  0x01uy;  0x5Auy;  0x45uy;  0x40uy;  0xDCuy;  0xDEuy;  0xA1uy; 
  0x58uy;  0x83uy;  0xCBuy;  0xBFuy;  0x31uy;  0x41uy;  0x2Duy;  0xF1uy;  0xDEuy;  0x1Cuy; 
  0xD4uy;  0x15uy;  0x2Buy;  0x91uy ]

let test14_expected : lbytes 64 =
  assert_norm(FStar.List.length test14_expected_list = 64);
  of_list test14_expected_list

(* test15_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E7F808182838485868788898A8B8C8D8E8F909192939495969798999A9B9C9D9E9FA0A1A2A3A4A5A6A7A8A9AAABACADAEAFB0B1B2B3B4B5B6B7B8B9BABBBCBDBEBFC0C1C2C3C4C5C6C7C8C9CACBCCCDCECFD0D1D2D3D4D5D6D7D8D9DADBDCDDDEDFE0E1E2E3E4E5E6E7E8E9EAEBECEDEEEFF0F1F2F3F4F5F6F7F8F9FAFBFCFDFEFF" *)
let test15_plaintext_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy;  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy; 
  0x28uy;  0x29uy;  0x2Auy;  0x2Buy;  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy; 
  0x32uy;  0x33uy;  0x34uy;  0x35uy;  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy; 
  0x3Cuy;  0x3Duy;  0x3Euy;  0x3Fuy;  0x40uy;  0x41uy;  0x42uy;  0x43uy;  0x44uy;  0x45uy; 
  0x46uy;  0x47uy;  0x48uy;  0x49uy;  0x4Auy;  0x4Buy;  0x4Cuy;  0x4Duy;  0x4Euy;  0x4Fuy; 
  0x50uy;  0x51uy;  0x52uy;  0x53uy;  0x54uy;  0x55uy;  0x56uy;  0x57uy;  0x58uy;  0x59uy; 
  0x5Auy;  0x5Buy;  0x5Cuy;  0x5Duy;  0x5Euy;  0x5Fuy;  0x60uy;  0x61uy;  0x62uy;  0x63uy; 
  0x64uy;  0x65uy;  0x66uy;  0x67uy;  0x68uy;  0x69uy;  0x6Auy;  0x6Buy;  0x6Cuy;  0x6Duy; 
  0x6Euy;  0x6Fuy;  0x70uy;  0x71uy;  0x72uy;  0x73uy;  0x74uy;  0x75uy;  0x76uy;  0x77uy; 
  0x78uy;  0x79uy;  0x7Auy;  0x7Buy;  0x7Cuy;  0x7Duy;  0x7Euy;  0x7Fuy;  0x80uy;  0x81uy; 
  0x82uy;  0x83uy;  0x84uy;  0x85uy;  0x86uy;  0x87uy;  0x88uy;  0x89uy;  0x8Auy;  0x8Buy; 
  0x8Cuy;  0x8Duy;  0x8Euy;  0x8Fuy;  0x90uy;  0x91uy;  0x92uy;  0x93uy;  0x94uy;  0x95uy; 
  0x96uy;  0x97uy;  0x98uy;  0x99uy;  0x9Auy;  0x9Buy;  0x9Cuy;  0x9Duy;  0x9Euy;  0x9Fuy; 
  0xA0uy;  0xA1uy;  0xA2uy;  0xA3uy;  0xA4uy;  0xA5uy;  0xA6uy;  0xA7uy;  0xA8uy;  0xA9uy; 
  0xAAuy;  0xABuy;  0xACuy;  0xADuy;  0xAEuy;  0xAFuy;  0xB0uy;  0xB1uy;  0xB2uy;  0xB3uy; 
  0xB4uy;  0xB5uy;  0xB6uy;  0xB7uy;  0xB8uy;  0xB9uy;  0xBAuy;  0xBBuy;  0xBCuy;  0xBDuy; 
  0xBEuy;  0xBFuy;  0xC0uy;  0xC1uy;  0xC2uy;  0xC3uy;  0xC4uy;  0xC5uy;  0xC6uy;  0xC7uy; 
  0xC8uy;  0xC9uy;  0xCAuy;  0xCBuy;  0xCCuy;  0xCDuy;  0xCEuy;  0xCFuy;  0xD0uy;  0xD1uy; 
  0xD2uy;  0xD3uy;  0xD4uy;  0xD5uy;  0xD6uy;  0xD7uy;  0xD8uy;  0xD9uy;  0xDAuy;  0xDBuy; 
  0xDCuy;  0xDDuy;  0xDEuy;  0xDFuy;  0xE0uy;  0xE1uy;  0xE2uy;  0xE3uy;  0xE4uy;  0xE5uy; 
  0xE6uy;  0xE7uy;  0xE8uy;  0xE9uy;  0xEAuy;  0xEBuy;  0xECuy;  0xEDuy;  0xEEuy;  0xEFuy; 
  0xF0uy;  0xF1uy;  0xF2uy;  0xF3uy;  0xF4uy;  0xF5uy;  0xF6uy;  0xF7uy;  0xF8uy;  0xF9uy; 
  0xFAuy;  0xFBuy;  0xFCuy;  0xFDuy;  0xFEuy;  0xFFuy ]

let test15_plaintext : lbytes 256 =
  assert_norm(FStar.List.length test15_plaintext_list = 256);
  of_list test15_plaintext_list

(* test15_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F" *)
let test15_key_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy;  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy; 
  0x28uy;  0x29uy;  0x2Auy;  0x2Buy;  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy; 
  0x32uy;  0x33uy;  0x34uy;  0x35uy;  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy; 
  0x3Cuy;  0x3Duy;  0x3Euy;  0x3Fuy ]

let test15_key : lbytes 64 =
  assert_norm(FStar.List.length test15_key_list = 64);
  of_list test15_key_list

(* test15_expected = "B72071E096277EDEBB8EE5134DD3714996307BA3A55AA4733D412ABBE28E909E10E57E6FBFB4EF53B3B960518294FF889A90829254412E2A60B85ADD07A3674F" *)
let test15_expected_list = List.Tot.map u8_from_UInt8 [
  0xB7uy;  0x20uy;  0x71uy;  0xE0uy;  0x96uy;  0x27uy;  0x7Euy;  0xDEuy;  0xBBuy;  0x8Euy; 
  0xE5uy;  0x13uy;  0x4Duy;  0xD3uy;  0x71uy;  0x49uy;  0x96uy;  0x30uy;  0x7Buy;  0xA3uy; 
  0xA5uy;  0x5Auy;  0xA4uy;  0x73uy;  0x3Duy;  0x41uy;  0x2Auy;  0xBBuy;  0xE2uy;  0x8Euy; 
  0x90uy;  0x9Euy;  0x10uy;  0xE5uy;  0x7Euy;  0x6Fuy;  0xBFuy;  0xB4uy;  0xEFuy;  0x53uy; 
  0xB3uy;  0xB9uy;  0x60uy;  0x51uy;  0x82uy;  0x94uy;  0xFFuy;  0x88uy;  0x9Auy;  0x90uy; 
  0x82uy;  0x92uy;  0x54uy;  0x41uy;  0x2Euy;  0x2Auy;  0x60uy;  0xB8uy;  0x5Auy;  0xDDuy; 
  0x07uy;  0xA3uy;  0x67uy;  0x4Fuy ]

let test15_expected : lbytes 64 =
  assert_norm(FStar.List.length test15_expected_list = 64);
  of_list test15_expected_list

(* test16_plaintext = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E7F808182838485868788898A8B8C8D8E8F909192939495969798999A9B9C9D9E9FA0A1A2A3A4A5A6A7A8A9AAABACADAEAFB0B1B2B3B4B5B6B7B8B9BABBBCBDBEBFC0C1C2C3C4C5C6C7C8C9CACBCCCDCECFD0D1D2D3D4D5D6D7D8D9DADBDCDDDEDFE0E1E2E3E4E5E6E7E8E9EAEBECEDEEEFF0F1F2F3F4F5F6F7F8F9FAFBFCFDFEFF000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F404142434445464748494A4B4C4D4E4F505152535455565758595A5B5C5D5E5F606162636465666768696A6B6C6D6E6F707172737475767778797A7B7C7D7E7F808182838485868788898A8B8C8D8E8F909192939495969798999A9B9C9D9E9FA0A1A2A3A4A5A6A7A8A9AAABACADAEAFB0B1B2B3B4B5B6B7B8B9BABBBCBDBEBFC0C1C2C3C4C5C6C7C8C9CACBCCCDCECFD0D1D2D3D4D5D6D7D8D9DADBDCDDDEDFE0E1E2E3E4E5E6E7E8E9EAEBECEDEEEFF0F1F2F3F4F5F6F7F8F9FAFBFCFDFEFF" *)
let test16_plaintext_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy;  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy; 
  0x28uy;  0x29uy;  0x2Auy;  0x2Buy;  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy; 
  0x32uy;  0x33uy;  0x34uy;  0x35uy;  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy; 
  0x3Cuy;  0x3Duy;  0x3Euy;  0x3Fuy;  0x40uy;  0x41uy;  0x42uy;  0x43uy;  0x44uy;  0x45uy; 
  0x46uy;  0x47uy;  0x48uy;  0x49uy;  0x4Auy;  0x4Buy;  0x4Cuy;  0x4Duy;  0x4Euy;  0x4Fuy; 
  0x50uy;  0x51uy;  0x52uy;  0x53uy;  0x54uy;  0x55uy;  0x56uy;  0x57uy;  0x58uy;  0x59uy; 
  0x5Auy;  0x5Buy;  0x5Cuy;  0x5Duy;  0x5Euy;  0x5Fuy;  0x60uy;  0x61uy;  0x62uy;  0x63uy; 
  0x64uy;  0x65uy;  0x66uy;  0x67uy;  0x68uy;  0x69uy;  0x6Auy;  0x6Buy;  0x6Cuy;  0x6Duy; 
  0x6Euy;  0x6Fuy;  0x70uy;  0x71uy;  0x72uy;  0x73uy;  0x74uy;  0x75uy;  0x76uy;  0x77uy; 
  0x78uy;  0x79uy;  0x7Auy;  0x7Buy;  0x7Cuy;  0x7Duy;  0x7Euy;  0x7Fuy;  0x80uy;  0x81uy; 
  0x82uy;  0x83uy;  0x84uy;  0x85uy;  0x86uy;  0x87uy;  0x88uy;  0x89uy;  0x8Auy;  0x8Buy; 
  0x8Cuy;  0x8Duy;  0x8Euy;  0x8Fuy;  0x90uy;  0x91uy;  0x92uy;  0x93uy;  0x94uy;  0x95uy; 
  0x96uy;  0x97uy;  0x98uy;  0x99uy;  0x9Auy;  0x9Buy;  0x9Cuy;  0x9Duy;  0x9Euy;  0x9Fuy; 
  0xA0uy;  0xA1uy;  0xA2uy;  0xA3uy;  0xA4uy;  0xA5uy;  0xA6uy;  0xA7uy;  0xA8uy;  0xA9uy; 
  0xAAuy;  0xABuy;  0xACuy;  0xADuy;  0xAEuy;  0xAFuy;  0xB0uy;  0xB1uy;  0xB2uy;  0xB3uy; 
  0xB4uy;  0xB5uy;  0xB6uy;  0xB7uy;  0xB8uy;  0xB9uy;  0xBAuy;  0xBBuy;  0xBCuy;  0xBDuy; 
  0xBEuy;  0xBFuy;  0xC0uy;  0xC1uy;  0xC2uy;  0xC3uy;  0xC4uy;  0xC5uy;  0xC6uy;  0xC7uy; 
  0xC8uy;  0xC9uy;  0xCAuy;  0xCBuy;  0xCCuy;  0xCDuy;  0xCEuy;  0xCFuy;  0xD0uy;  0xD1uy; 
  0xD2uy;  0xD3uy;  0xD4uy;  0xD5uy;  0xD6uy;  0xD7uy;  0xD8uy;  0xD9uy;  0xDAuy;  0xDBuy; 
  0xDCuy;  0xDDuy;  0xDEuy;  0xDFuy;  0xE0uy;  0xE1uy;  0xE2uy;  0xE3uy;  0xE4uy;  0xE5uy; 
  0xE6uy;  0xE7uy;  0xE8uy;  0xE9uy;  0xEAuy;  0xEBuy;  0xECuy;  0xEDuy;  0xEEuy;  0xEFuy; 
  0xF0uy;  0xF1uy;  0xF2uy;  0xF3uy;  0xF4uy;  0xF5uy;  0xF6uy;  0xF7uy;  0xF8uy;  0xF9uy; 
  0xFAuy;  0xFBuy;  0xFCuy;  0xFDuy;  0xFEuy;  0xFFuy;  0x00uy;  0x01uy;  0x02uy;  0x03uy; 
  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy;  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy; 
  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy;  0x14uy;  0x15uy;  0x16uy;  0x17uy; 
  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy;  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy; 
  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy;  0x28uy;  0x29uy;  0x2Auy;  0x2Buy; 
  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy;  0x32uy;  0x33uy;  0x34uy;  0x35uy; 
  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy;  0x3Cuy;  0x3Duy;  0x3Euy;  0x3Fuy; 
  0x40uy;  0x41uy;  0x42uy;  0x43uy;  0x44uy;  0x45uy;  0x46uy;  0x47uy;  0x48uy;  0x49uy; 
  0x4Auy;  0x4Buy;  0x4Cuy;  0x4Duy;  0x4Euy;  0x4Fuy;  0x50uy;  0x51uy;  0x52uy;  0x53uy; 
  0x54uy;  0x55uy;  0x56uy;  0x57uy;  0x58uy;  0x59uy;  0x5Auy;  0x5Buy;  0x5Cuy;  0x5Duy; 
  0x5Euy;  0x5Fuy;  0x60uy;  0x61uy;  0x62uy;  0x63uy;  0x64uy;  0x65uy;  0x66uy;  0x67uy; 
  0x68uy;  0x69uy;  0x6Auy;  0x6Buy;  0x6Cuy;  0x6Duy;  0x6Euy;  0x6Fuy;  0x70uy;  0x71uy; 
  0x72uy;  0x73uy;  0x74uy;  0x75uy;  0x76uy;  0x77uy;  0x78uy;  0x79uy;  0x7Auy;  0x7Buy; 
  0x7Cuy;  0x7Duy;  0x7Euy;  0x7Fuy;  0x80uy;  0x81uy;  0x82uy;  0x83uy;  0x84uy;  0x85uy; 
  0x86uy;  0x87uy;  0x88uy;  0x89uy;  0x8Auy;  0x8Buy;  0x8Cuy;  0x8Duy;  0x8Euy;  0x8Fuy; 
  0x90uy;  0x91uy;  0x92uy;  0x93uy;  0x94uy;  0x95uy;  0x96uy;  0x97uy;  0x98uy;  0x99uy; 
  0x9Auy;  0x9Buy;  0x9Cuy;  0x9Duy;  0x9Euy;  0x9Fuy;  0xA0uy;  0xA1uy;  0xA2uy;  0xA3uy; 
  0xA4uy;  0xA5uy;  0xA6uy;  0xA7uy;  0xA8uy;  0xA9uy;  0xAAuy;  0xABuy;  0xACuy;  0xADuy; 
  0xAEuy;  0xAFuy;  0xB0uy;  0xB1uy;  0xB2uy;  0xB3uy;  0xB4uy;  0xB5uy;  0xB6uy;  0xB7uy; 
  0xB8uy;  0xB9uy;  0xBAuy;  0xBBuy;  0xBCuy;  0xBDuy;  0xBEuy;  0xBFuy;  0xC0uy;  0xC1uy; 
  0xC2uy;  0xC3uy;  0xC4uy;  0xC5uy;  0xC6uy;  0xC7uy;  0xC8uy;  0xC9uy;  0xCAuy;  0xCBuy; 
  0xCCuy;  0xCDuy;  0xCEuy;  0xCFuy;  0xD0uy;  0xD1uy;  0xD2uy;  0xD3uy;  0xD4uy;  0xD5uy; 
  0xD6uy;  0xD7uy;  0xD8uy;  0xD9uy;  0xDAuy;  0xDBuy;  0xDCuy;  0xDDuy;  0xDEuy;  0xDFuy; 
  0xE0uy;  0xE1uy;  0xE2uy;  0xE3uy;  0xE4uy;  0xE5uy;  0xE6uy;  0xE7uy;  0xE8uy;  0xE9uy; 
  0xEAuy;  0xEBuy;  0xECuy;  0xEDuy;  0xEEuy;  0xEFuy;  0xF0uy;  0xF1uy;  0xF2uy;  0xF3uy; 
  0xF4uy;  0xF5uy;  0xF6uy;  0xF7uy;  0xF8uy;  0xF9uy;  0xFAuy;  0xFBuy;  0xFCuy;  0xFDuy; 
  0xFEuy;  0xFFuy ]

let test16_plaintext : lbytes 512 =
  assert_norm(FStar.List.length test16_plaintext_list = 512);
  of_list test16_plaintext_list

(* test16_key = "000102030405060708090A0B0C0D0E0F101112131415161718191A1B1C1D1E1F202122232425262728292A2B2C2D2E2F303132333435363738393A3B3C3D3E3F" *)
let test16_key_list = List.Tot.map u8_from_UInt8 [
  0x00uy;  0x01uy;  0x02uy;  0x03uy;  0x04uy;  0x05uy;  0x06uy;  0x07uy;  0x08uy;  0x09uy; 
  0x0Auy;  0x0Buy;  0x0Cuy;  0x0Duy;  0x0Euy;  0x0Fuy;  0x10uy;  0x11uy;  0x12uy;  0x13uy; 
  0x14uy;  0x15uy;  0x16uy;  0x17uy;  0x18uy;  0x19uy;  0x1Auy;  0x1Buy;  0x1Cuy;  0x1Duy; 
  0x1Euy;  0x1Fuy;  0x20uy;  0x21uy;  0x22uy;  0x23uy;  0x24uy;  0x25uy;  0x26uy;  0x27uy; 
  0x28uy;  0x29uy;  0x2Auy;  0x2Buy;  0x2Cuy;  0x2Duy;  0x2Euy;  0x2Fuy;  0x30uy;  0x31uy; 
  0x32uy;  0x33uy;  0x34uy;  0x35uy;  0x36uy;  0x37uy;  0x38uy;  0x39uy;  0x3Auy;  0x3Buy; 
  0x3Cuy;  0x3Duy;  0x3Euy;  0x3Fuy ]

let test16_key : lbytes 64 =
  assert_norm(FStar.List.length test16_key_list = 64);
  of_list test16_key_list

(* test16_expected = "31952478E1B6229B6BCA296C643A3FDBE4AA2C2F7FEA466675453D5F7F09427021A77B8625C78070C0F7CE564D8D257D7EB36495BE76950C31A1A7D80FF8B1B4" *)
let test16_expected_list = List.Tot.map u8_from_UInt8 [
  0x31uy;  0x95uy;  0x24uy;  0x78uy;  0xE1uy;  0xB6uy;  0x22uy;  0x9Buy;  0x6Buy;  0xCAuy; 
  0x29uy;  0x6Cuy;  0x64uy;  0x3Auy;  0x3Fuy;  0xDBuy;  0xE4uy;  0xAAuy;  0x2Cuy;  0x2Fuy; 
  0x7Fuy;  0xEAuy;  0x46uy;  0x66uy;  0x75uy;  0x45uy;  0x3Duy;  0x5Fuy;  0x7Fuy;  0x09uy; 
  0x42uy;  0x70uy;  0x21uy;  0xA7uy;  0x7Buy;  0x86uy;  0x25uy;  0xC7uy;  0x80uy;  0x70uy; 
  0xC0uy;  0xF7uy;  0xCEuy;  0x56uy;  0x4Duy;  0x8Duy;  0x25uy;  0x7Duy;  0x7Euy;  0xB3uy; 
  0x64uy;  0x95uy;  0xBEuy;  0x76uy;  0x95uy;  0x0Cuy;  0x31uy;  0xA1uy;  0xA7uy;  0xD8uy; 
  0x0Fuy;  0xF8uy;  0xB1uy;  0xB4uy ]

let test16_expected : lbytes 64 =
  assert_norm(FStar.List.length test16_expected_list = 64);
  of_list test16_expected_list


//
// Main
//


#set-options "--z3rlimit 400"

//
// Main
//

let blake2s_test num (plain:bytes{Seq.length plain <= max_size_t}) (key:bytes{Seq.length key <= 32}) expected =
  IO.print_string ("\n\nTEST Blake2s "^(string_of_int num)^":");

  let result : lbytes 32 =
    Spec.Blake2.blake2s plain (Seq.length key) key 32
  in
  let result2 = for_all2 (fun a b -> uint_to_nat #U8 a = uint_to_nat #U8 b) expected result in

 if result2 then begin  IO.print_string "\nSuccess!\n"; true end
 else begin IO.print_string "\nFailure :(\n";

  IO.print_string "\n2. Result  : ";
  List.iter (fun a -> IO.print_uint8 (u8_to_UInt8 a)) (to_list result);

  IO.print_string "\n2. Expected: ";
  List.iter (fun a -> IO.print_uint8 (u8_to_UInt8 a)) (to_list expected);
 false end


let blake2b_test num (plain:bytes{Seq.length plain <= max_size_t}) (key:bytes{Seq.length key <= 64}) expected =
  IO.print_string ("\n\nTEST Blake2b "^(string_of_int num)^":");

  let result : lbytes 64 =
    Spec.Blake2.blake2b plain (Seq.length key) key 64
  in
  let result2 = for_all2 (fun a b -> uint_to_nat #U8 a = uint_to_nat #U8 b) expected result in

 if result2 then begin  IO.print_string "\nSuccess!\n"; true end
 else begin IO.print_string "\nFailure :(\n";

  IO.print_string "\n2. Result  : ";
  List.iter (fun a -> IO.print_uint8 (u8_to_UInt8 a)) (to_list result);

  IO.print_string "\n2. Expected: ";
  List.iter (fun a -> IO.print_uint8 (u8_to_UInt8 a)) (to_list expected);
 false end


let test () =
  let emp_key : lbytes 0 = (assert_norm (List.Tot.length ([] <: list uint8)<= max_size_t); of_list []) in
  let result1 = blake2s_test 1 test1_plaintext emp_key test1_expected in
  let result2 = blake2s_test 2 test2_plaintext test2_key test2_expected in
  let result3 = blake2s_test 3 test3_plaintext test3_key test3_expected in
  let result4 = blake2s_test 4 test4_plaintext test4_key test4_expected in
  let result7 = blake2s_test 7 test7_plaintext test7_key test7_expected in
  let result8 = blake2s_test 8 test8_plaintext test8_key test8_expected in
  let result9 = blake2s_test 9 test9_plaintext test9_key test9_expected in
  let result10 = blake2s_test 10 test10_plaintext test10_key test10_expected in
  let result11 = blake2s_test 11 test11_plaintext test11_key test11_expected in

  let result5 = blake2b_test 5 test5_plaintext emp_key test5_expected in
  let result6 = blake2b_test 6 test6_plaintext test6_key test6_expected in
  let result12 = blake2b_test 12 test12_plaintext test12_key test12_expected in
  let result13 = blake2b_test 13 test13_plaintext test13_key test13_expected in
  let result14 = blake2b_test 14 test14_plaintext test14_key test14_expected in
  let result15 = blake2b_test 15 test15_plaintext test15_key test15_expected in
  let result16 = blake2b_test 16 test16_plaintext test16_key test16_expected in
  //
  //
  // RESULT
  //
  if result1 && result2 && result3 && result4 && result5 && result6 &&
     result7 && result8 && result9 && result10 && result11 && result12 &&
     result13 && result14 && result15 && result16 then
  begin IO.print_string "\n\nAll tests successful !\n"; true end
  else begin IO.print_string "\n\nSome test failed !\n"; false end
